forall a: forall b:
forall Q:a->b:
O:a,b < Q